Nuprl Lemma : R-realizes_wf
11,40
postcript
pdf
R
:es_realizer{i:l},
P
:(event_system{i:l}
prop{i':l}).
R-realizes{i:l}(
R
;
es
.
P
(
es
))
prop{i'':l}
latex
Definitions
P
Q
,
P
Q
,
x
(
s
)
,
R-realizes{i:l}(
R
;
es
.
P
(
es
))
,
t
T
,
prop{i:l}
,
x
:
A
.
B
(
x
)
Lemmas
es
realizer
wf
,
R-consistent
wf
,
event
system
wf
,
R-Feasible
wf
origin
R:es_realizer{i:l}, P:(event_system{i:l}
prop{i':l}).
prop{i'':l} R:es_realizer{i:l}, P:(event_system{i:l}prop{i':l}).
prop{i'':l} 
Q
Q Tx:A. B(x)